Closed Convex Cones in LP

I was formalizing some linear programming in Lean and came across one of the most surprisingly difficult to prove theorems.

Theorem 1

Let \(A : \mathbb{R}^m \to \mathbb{R}^n\) be a linear transformation. Then the set \[ \{ A x \: : \: x \ge 0 \} \] is closed in \(\mathbb{R}^n\).

The naive topological approach doesn’t work as this theorem is no longer true if we replace \(A\) by an arbitrary continuous map or if we replace \(x \ge 0\) by an arbitrary closed set.

This theorem is obviously true if \(A\) is invertible. The proof then relies on the fact that \[ \{ A x \: : \: x \ge 0 \} = \bigcup_i \{ A_i x \: : \: x \ge 0 \} \] where \(A_i\) are the submatrices of \(A\) formed using the linearly independent columns. This fact itself is surprisingly hard to prove and relies on Caratheodory’s theorem for vectors in a cone.